The division and modulo operations are fundamental in computer science and mathematics. In this article, we will show how to prove some properties of these operations using the recursive definition of the division and modulo operations. We will use the Scala Stainless tool to verify these properties.
Given integers and where , the division algorithm determines integers and such that:
Some properties of the division and module can be proved using the recursive definition of the division and module operations.
The recursive definition of the division and module operations are:
We define such that:
The solved are those where the remainder satisfies:
We can see the described recursive definition on Scala, simplified as follows:
case class Div(a: BigInt, b: BigInt, div: BigInt, mod: BigInt ) {
require(div * b + mod == a)
require(b != 0)
def isValid: Boolean = div * b + mod == a
def isFinal: Boolean = if (b > 0) mod < b && mod >= 0 else mod < -b && mod >= 0
def solve: Div = if (this.isFinal) this else ( if (mod > 0) reduceMod else increaseMod )
def reduceMod: Div = {
require(mod >= 0)
decreases(mod)
if isFinal then this else (if (b > 0) ModLessB else ModPlusB).reduceMod
}.ensuring(res => res.isFinal && res.isValid)
def increaseMod: Div = {
val absB = if (b > 0) b else -b
require(mod < 0)
decreases(-mod)
if isFinal this else (if (b > 0) ModPlusB else ModLessB).increaseMod
}.ensuring(res => res.isFinal && res.isValid)
def ModPlusB: Div = Div(a, b, div - 1, mod + b)
def ModLessB: Div = Div(a, b, div + 1, mod - b)
override def equals(obj: Any): Boolean = {
obj match {
case that: Div =>
( that.a == this.a &&
that.b == this.b &&
that.div == this.div &&
that.mod == this.mod ) ||
( that.solve == this.solve )
case _ => false
}
}
}
As we can see in the class Calc, we can define the division and module operations by extracting these properties from the solved as follows:
def div(a: BigInt, b: BigInt): BigInt = {
require(b != 0)
check(a == 0 * b + a)
val result = Div(a, b, 0, a)
val solved = result.solve
solved.div
}
def mod(a: BigInt, b: BigInt): BigInt = {
require(b != 0)
check(a == 0 * b + a)
val result = Div(a, b, 0, a)
val solved = result.solve
solved.mod
}
If the dividend is smaller than the divisor, the result of the modulos operation should be the dividend value and the division result should be zero.
We can check that since is the final solution for the division operation. That verification is available in ModSmallDividend and simplified below:
def modSmallDividend(a: BigInt, b: BigInt): Boolean = {
require(b != 0)
require(b > a)
require(a >= 0)
val x = Div(a, b, 0, a)
check(x.isFinal)
check(x == x.solve)
check(x.mod == a)
check(x.div == 0)
check(Calc.mod(a, b) == x.mod)
check(Calc.div(a, b) == 0)
Calc.mod(a, b) == a &&
Calc.div(a, b) == 0
}.holds
The modulo of every number by itself is zero and the division of every number by itself is one.
We can prove this property using the recursive definition of the division and module operations. As the following simplified version of the long proof code example:
def longProof(n: BigInt): Boolean = {
require(n != 0)
check(!Div(a = n, b = n, div = 0, mod = n).isFinal)
if (n > 0) {
check(
Div(a=n, b=n, div=0, mod=n).solve ==
Div(a=n, b=n, div=0, mod=n).reduceMod.solve ==
Div(a=n, b=n, div=0, mod=n).ModLessB.reduceMod ==
Div(a=n, b=n, div=1, mod=0).reduceMod ==
Div(a=n, b=n, div=1, mod=0)
)
// since
check(Div(a=n, b=n, div=1, mod=0).isFinal)
} else {
check(
Div(a=n, b=n, div=0, mod=n).solve ==
Div(a=n, b=n, div=0, mod=n).increaseMod.solve ==
Div(a=n, b=n, div=0, mod=n).ModPlusB.increaseMod ==
Div(a=n, b=n, div=1, mod=0)
)
// since
check(Div(a=n, b=n, div=1, mod=0).isFinal)
}
Div(a=n, b=n, div=0, mod=n).solve == Div(a=n, b=n, div=1, mod=0)
}.holds
But we don't need to manually do all these transformations. Scala Stainless can verify that property holds in ModIdentity with no issues as follows:
def modIdentity(a: BigInt): Boolean = {
require(a != 0)
Calc.mod(a, a) == 0
}.holds
Similary, in the next sections, we will prove other properties of the division and module operations using only the amount of evidences required to Scala Stainless to verify that they hold.
As proved in MoreDivLessMod and LessDivMoreMod and shown in a simplified version in the code below, the division result is the same for the same dividend and divisor, regardless of the div and mod values, as long .
def MoreDivLessMod(a: BigInt, b: BigInt, div: BigInt, mod: BigInt): Boolean = {
require(b != 0)
require(div * b + mod == a)
val div1 = Div(a, b, div, mod)
val div2 = Div(a, b, div + 1, mod - b)
if (div1.isFinal) check(!div2.isFinal && div2.solve == div1.solve)
if (div2.isFinal) check(!div1.isFinal && div1.solve == div2.solve)
if (div1.mod < 0) {
check(div1.solve == div1.increaseMod)
if (b > 0) check(div2.solve == div2.increaseMod == div1.increaseMod == div1.solve)
else check(div1.solve == div1.increaseMod == div2.solve)
}
if (div1.mod > 0 && ! div1.isFinal && ! div2.isFinal) {
if (b > 0 ) {
check(div2.mod < div1.mod)
check(div1.solve == div1.reduceMod == div2.solve)
} else {
check(div2.mod > div1.mod)
check(div2.solve == div2.reduceMod == div1.solve)
}
}
check(div1.solve == div2.solve)
Div(a,b, div + 1, mod - b).solve.mod == Div(a,b, div, mod).solve.mod
}.holds
def LessDivMoreMod(a: BigInt, b: BigInt, div: BigInt, mod: BigInt): Boolean = {
require(b != 0)
require(div * b + mod == a)
check(a == div * b + mod)
check(a == (div - 1) * b + (mod + b))
MoreDivLessMod(a, b, div - 1, mod + b)
Div(a, b, div, mod).solve == Div(a, b, div - 1, mod + b).solve
}.holds
As a directly consequence of these properties, we can extend the Div with the following properties:
There is only one single remainder value for every pair.
in other words:
For every pair, with any , there is always the same and single solution for the division operation. That is proved in the unique remainder property as simplified below:
def modUnique(a: BigInt, b: BigInt, divx: BigInt, modx: BigInt, divy: BigInt, mody: BigInt): Boolean = {
require(divx * b + modx == a)
require(divy * b + mody == a)
val x = Div(a, b, divx, modx)
val y = Div(a, b, divy, mody)
if (divx == divy) {
check(modx == mody)
check(x == y)
}
if (divx < divy) {
check(modx > mody)
val next = Div(a, b, divx + 1, modx - b)
check(x.solve == next.solve)
modUnique(a, b, divx + 1, modx - b, divy, mody)
}
if (divx > divy) {
check(modx < mody)
val next = Div(a, b, divx - 1, modx + b)
check(x.solve == next.solve)
modUnique(a, b, divx - 1, modx + b, divy, mody)
}
check(x.solve == y.solve)
Div(a, b, divx, modx).solve == Div(a, b, divy, mody).solve
}.holds
The proof of the modulo idempotence property is available in the ModIdempotence as follows:
def modIdempotence(a: BigInt, b: BigInt): Boolean = {
require(b != 0)
require(a >= 0)
val div = Div(a, b, 0, a)
val absB = if (b < 0) -b else b
val solved = div.solve
check(solved.isFinal)
check(solved.b == div.b)
check(solved.a == div.a)
check(absB > 0)
check(solved.mod < absB)
check(solved.mod >= 0)
val result = solved.mod
check(result <= a)
check(result < absB)
check(result == Calc.mod(a, b))
check(Calc.mod(result, b) == result)
check(Calc.mod(a, b) == Calc.mod(result, b))
Calc.mod(a, b) == Calc.mod(Calc.mod(a, b), b)
}.holds
These properties are proved in the ModOperations, as simplified as follows:
def modAdd(a: BigInt, b: BigInt, c: BigInt): Boolean = {
require(b != 0)
val absB = if (b < 0) -b else b
val x = Div(a, b, 0, a)
val solvedX = x.solve
check(solvedX.mod < absB)
check(solvedX.a == a && solvedX.b == b)
check(solvedX.a == solvedX.b * solvedX.div + solvedX.mod) // by definition
check(solvedX.a - solvedX.b * solvedX.div == solvedX.mod) // transposing solvedX.b * solvedX.div to the left side
val y = Div(c, b, 0, c)
val solvedY = y.solve
check(solvedY.mod < absB)
check(solvedY.a == c && solvedY.b == b)
check(solvedY.a == solvedY.b * solvedY.div + solvedY.mod) // by definition
check(solvedY.a - solvedY.b * solvedY.div == solvedY.mod) // transposing solvedY.b * solvedY.div to the left side
val xy = Div(a + c, b, 0, a + c) // xy is the division of a + c by b
val solvedXY = xy.solve
check(solvedXY.mod < absB)
check(solvedXY.a == a + c)
check(solvedXY.b == b)
check(solvedXY.a == solvedXY.b * solvedXY.div + solvedXY.mod)
check(a + c == b * solvedXY.div + solvedXY.mod) // by definition
val z = Div(solvedX.mod + solvedY.mod, b, 0, solvedX.mod + solvedY.mod)
check(z.a == z.b * z.div + z.mod) // by definition
check(z.mod == solvedX.mod + solvedY.mod)
val solvedZ = z.solve
check(solvedZ.mod < absB)
check(modUniqueDiv(z, solvedZ))
check(z.solve.mod == solvedZ.mod)
check(solvedX.mod + solvedY.mod == b * solvedZ.div + solvedZ.mod)
check(solvedX.a - solvedX.b * solvedX.div + solvedY.a - solvedY.b * solvedY.div == b * solvedZ.div + solvedZ.mod)
check(a - b * solvedX.div + c - b * solvedY.div == b * solvedZ.div + solvedZ.mod)
check(a + c == b * solvedZ.div + b * solvedX.div + b * solvedY.div + solvedZ.mod) // transposing b * solvedX.div + b * solvedY.div to the left side
val bigDiv = solvedZ.div + solvedX.div + solvedY.div
check(a + c == b * bigDiv + solvedZ.mod)
val w = Div(a + c, b, bigDiv, solvedZ.mod) // is valid since a + c = b * bigDiv + solvedZ.mod
check(solvedZ.mod < absB)
check(w.mod == solvedZ.mod)
check(w.isFinal && w.solve == w)
/* calling the proof of the property Module Plus Multiples of Divisor
* mod(a + m * b, b) = mod(a, b)
* described previously
*/
DivModAdditionAndMultiplication.ATimesBSameMod(a + c, b, bigDiv)
check(Calc.mod(a + c,b) == Calc.mod( a + c + b * bigDiv, b ))
check(w.a == xy.a && w.b == xy.b)
/* calling the proof of the property Unique Remainder
* mod(a, b) = mod(a, b)
* described previously
*/
check(modUniqueDiv(w, xy))
check(w.solve == xy.solve)
check(w.solve.mod == xy.solve.mod == Calc.mod(a+c,b) == solvedZ.mod)
Calc.mod(a + c, b) == Calc.mod(Calc.mod(a, b) + Calc.mod(c, b), b) &&
Calc.div(a + c, b) == Calc.div(a, b) + Calc.div(c, b) + Calc.div(Calc.mod(a, b) + Calc.mod(c, b), b)
}.holds
def modLess(a: BigInt, b: BigInt, c: BigInt): Boolean = {
require(b != 0)
modAdd(a - c, b, c)
Calc.mod(a - c, b) == Calc.mod(Calc.mod(a, b) - Calc.mod(c, b), b) &&
Calc.div(a - c, b) == Calc.div(a, b) - Calc.div(c, b) + Calc.div(Calc.mod(a, b) - Calc.mod(c, b), b)
}.holds
The division and module operations are fundamental in computer science and mathematics. In this article, we have shown how to prove some properties of these operations using the recursive definition of the division and modulo operations. We used the Scala Stainless tool to verify these properties. The properties proved in this article were: